Labeling techniques and typed fixed-point operators

John C. Mitchell, Department of Computer Science, Stanford University

My Hoang, SAP Technology, Inc., 950 Tower Lane, 16th Floor, Foster City, CA 94404, my.hoang@sap-ag.de

Brian Howard, Department of Computing & Information Sciences, Kansas State University, bhoward@cis.ksu.edu

Abstract

Labeling techniques for untyped lambda calculus were developed by Levy, Hyland, Wadsworth and others in the 1970's. A typical application is the proof of confluence from finiteness of developments: by labeling each subterm with an natural number indicating the maximum number of times this term may participate in a reduction step, we obtain a strongly-normalizing approximation of beta,eta-reduction. Confluence then follows by a syntactic ``compactness" argument (repeated in the introduction of this paper).

This paper presents applications of labeling to typed lambda calculi with fixed-point operators, including confluence and completeness of left-most reduction for PCF (an ``applied'' lambda calculus with fixed-point operators and numeric and boolean operations) and a confluence proof for a variant of typed lambda calculus with subtyping. Labeling is simpler for typed calculi than untyped calculi because the fixed-point operator is the only source of nontermination. We can also use the method of logical relations for the labeled typed calculus, extended with basic operations like addition and conditional. This method would not apply to untyped lambda calculus.